COMMENT ⊗   VALID 00009 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Preliminary documentation on type system.
C00016 00003	Typed expressions
C00036 00004	List of constructors for typed expressions
C00042 00005	List of type system operations:
C00052 00006	Compiling typed code.
C00054 00007	The other type constructors: list and union.
C00064 00008	File management: the  "require" and "doneloading" operations.
C00066 00009	Use of the type system in the SSA environment, and pointers to examples.
C00075 ENDMK
C⊗;
Preliminary documentation on type system.

The notion of  "type" on  which the  system is  based is  similar but  not
identical to conventional notions of type used in other data type systems.
For our purposes, a type may be  defined as a class of (abstact)  objects,
together with  a selection  of a  scheme for  representing those  abstract
objects by concrete objects.  Here, "concrete" and "abstract" are relative
terms, the concrete objects will in general  belong to a type which is  in
turn represented by yet more concrete  objects, and so forth.  The end  of
this chain going  from abstract  to concrete  is the  primitive type,  the
members of which are directly represented in the base programming language
(here, maclisp).

To state matters formally, a type  can be defined recursively as  follows:
A type  tp is  either  a primitive  type (see  below)  or a  triple  whose
components are designated CLASS(tp),REPTYP(tp), and REPMAP(tp);  CLASS(tp)
is a class of "abstract"  objects,(the "elements" of the type)  REPTYP(tp)
["representation type"] is a type whose  class is the class of  "concrete"
objects which  represent  elements of tp,  and REPMAP(tp)  is  the
representation map which takes each element of REPTYP(tp) into  the
object which it represents. REPMAPs may  be partial; we don't force  every
[better: "REPMAPs need not be onto"]
"concrete" object to represent an "abstract" object.

In the type system,  the representation maps are  posited but not  defined
(as a consequence,  there is  no need for  the representation  maps to  be
computable in  any sense.)   In  the end,  only  operations on  the  fully
concrete primitive types are implemented.  The purpose of the type  system
is to describe the manner in  which these concrete operations are  related
to the abstract operations which they represent.


The "primitive"  types  supported  in the  current  system  are:   fixnum,
flonum, and lispob,  and types  built up from  these by  the function,tuple,
list, and union
constructors (see below).   A lispob is a  lisp object of  arbitrary
kind.  From a formal point of view, these are simply classes for which  no
representations need be  given, since they  are implemented directly  in
the underlying language. For uniformity, however, it will be convenient to
stipulate that, for  each primitive  type ptyp, reptyp(ptyp)  = ptyp,  and
repmap(ptyp) = the identity map on  ptyp (ie elements of a primitive  type
represent themselves).

There are also four constructors for building up compound types from simple
types:tuple,function,union,list.  
The first two will be described here, and the others left to
a separate section.
If tp1 .  . tpn are  types, then tpt  = tuple(tp1 .  . .tpn) is  a
type, and so is function(tp1 . . tpn).  The meanings of these constructors
as they apply to the classes of the types is exactly conventional - but we
still need to define the effects of the constructors on the representation
types  and  representation   maps  associated  with   the  types.    These
definitions also follow a conventional pattern.  The definitions are given
formally in  the next  paragraph, but  can probably  be skipped  by  those
interested only  in  the  use of  the  type  system, and  not  its  formal
underpinnings.

Let tpt = tuple(tp1 . ..tpn).
Then, class(tpt) = class(tp1) x class(tp2) . . class(tpn) [where x = cross product],
[better: Cartesian product]
If tp1 . . tpn are primitive, then so is tpt, so we don't need to specify
further how it is represented. Otherwise,
reptyp(tpt) = reptyp(tp1) x ... reptyp(tpn), and
repmap(tpt) maps the tuple <y1 . . . yn> into the tuple 
<repmap(tp1)(y1) . . . repmap(tp1)(yn)>.
Second, there is the function constructor:
Let tpf = function(tp0,tp1, . . tpn). Then 
class(tpf) = the class of partial functions from class(tp1) x . . class(tpn) to tp0.
If tp0 . . tpn are primitive, then function(tp0 . . tpn) is also primitive.
Otherwise, reptyp(tpf) =  function(reptyp(tp0) . . . reptyp(tpn)).
To define repmap(tpf), let f be an element
 function(reptyp(tp0) . . . reptyp(tpn)).  The element g (if any) of 
function(tp0 . . tpn) which f represents is defined as follows. Let
<a1, . . . an> be elements of reptyp(tp1)  . . . reptyp(tpn) respectively,
and let <b1 . . . bn> be the objects in tp1 . . tpn which a1 . . an
represent. (ie bi = repmap(tpi)(ai)).  Then g(b1 . . bn) is defined
to be repmap(tp0)(f(a1 . . an)) - that is, g(b1 . . bn) takes as value
the object represented by f(a1 . . an).  This is an unambiguous definition
of g at <b1 . . bn> so long as b1 ... bn are not represented by two 
sets of values <a1 . . an>, <a1' . . an'> on which f takes values
v=f(a1 . . an), v'=f(a1' . . an') which represent different elements
of tp0.  If this problem does arise for any b1 . . . bn, then
g (ie repmap(function(tp0,. . tpn))(f)) is taken to be undefined.


Before going further, it is worthwhile mentioning the manner in which  the
type system is implemented within the lisp environment.  All type  related
operations are lisp functions (which may be exprs, fexprs, or macros), and
are represented by lisp symbols or expressions.  Executing type operations
is a matter of calling the lisp functions which perform them; there is  no
modification in the Lisp top level.   Several of the type operations  have
the effect of assigning types, or code, to lisp symbols.  These operations
affect the global state; the typing information associated with symbols is
generally kept on their property lists.

A type expression is either a lisp symbol which has been defined
as a type, or an expression of one of the forms

("function" tp0 tp1 . . tpn) [designating the type of functions from
				from tp1 x tp2 . . tpn into tp0]

("tuple" tp1 . . tpn)  [designating the type of tuples of objects
			of the given types]
("union" tp1 . . tpn)

("list" tp1 . . .tpn)



The main operations in the type system are as follows. (Conventions:
lisp symbols will be desginated by syntactic variables of the form
"sym"*, and type expressions 
by "tp"*.  The system is set up to be used from cgol - though this
is not a requirement - and accordingly, we give the cgol syntax for
all operations in what follows.) 

Type introduction operations:

tp represents sym	introduces sym as a new type represented by objects
				of type tp. represents is an infix fexpr.


dftyp(sym,tp)		introduces sym as an abreviation for the type
			tp.  This is an abreviatin in the strict sense;
			after a dftyp, any use of the symbol will produce
			the same effects as the use of what it abreviates.

Type assignment operations, and definition of typed functions.

"settyp(sym,typexpression)" 

			Assigns the type designated by typexpression
			to the symbol sym. 

"dftfun(sym(varlist),body)"  

			Defines sym as a typed function. Varlist is a list of
			typed variables, and body is a typed expression.
			(more about typed expressions later).

"mkinjmap(tp1,tp2,f)"

			Specifies f as an "injection map" (meaning
			preserving map)
			from type tp1 to type tp2.  
			f should be of type function(reptyp(tp2),reptyp(tp1)),
			and should have the property that for each
			x in reptyp(tp1), repmap(tp1)(x) = rempap(tp2)(f(x)) -
			that is x, f(x) should represent the same abstract object.
			Injection maps
			are used in type coersion.
			Restriction: tp1,tp2 should both be "named" types:
			types which have been introduced by the mktupletyp
			or "represents" operations, and which are
			given by lisp symbols rather than type expresssions.


Evaluation of typed expressions:

"teval(exp)"		Evaluates exp as a typed expression, and returns
			a typed result.


These, operations, together with a few variants introduced later,  constitute
the complete set of operations of the type system.  What remains to be explained
is what a "typed expression" is.

Typed expressions

A typed expression in this system  takes a conventional form; like a  lisp
expression, it is built up by function application and the application  of
special constructors (such as "cond", and "prog") from atomic expressions.
The difference  to  ordinary lisp  is  just  that 
each typed  expression
has an associated type.  The type  is generally computed recursively from  the
types  of  its  constituents of the expression,  
rather  than  explicitly  given  with   the
expression itself.  
The  types  assigned  to
functions and the  types assigned  to their  arguments must  agree in  the
appropriate sense,  and  also  that  certain  type  restrictions  must  be
observed in the use  of the special  constructors.  
Just  as a  lisp expression denotes  (evaluates to)  a
lisp object, so a typed expression denotes an object - an object which  is
an element of the type of the expression.  

The type of a typed expression is defined inductively as follows.

(1) Base case: typing of  variables and constants.  In typed  expressions,
the variable lists of the the binding constructs lambda, do, and prog, are
lists of TYPED variables.  A typed  variable is an expression of the  form
"(type var tp)", in LISP syntax, where var  is a lisp symbol, and tp is  a
type expression.  In  the type  system ":" has  been defined  as an  infix
operator whose meaning is "type", so  that the cgol syntax for "(type  var
tp)" is "var:tp".   Not all  variables in a  typed variable  list need  be
explicitly typed;  those  which are  not  are automatically  assigned  the
primitive type LISPOB (lisp object).

Now, the type of an atom occuring in a typed expression is:
(1) "fixnum" if the atom is a fixnum constant
(2) "flonum" if the atom is a flonum constant
(3) tp       if the atom is bound by a binding construct in whose
	     variable list the atom has been assigned the type tp
(4) tp	     if the atom is a symbol which has been assigned
	     the type tp by the settyp operation given above.
(5) LISPOB   other wise

The reader will note that symbols (both in binding lists, and elsewhere in
typed expressions)  which have  not been  explicitly assigned  a type  are
assigned the type  LISPOB.  This  rule goes further:  any lisp  expression
with which no  typing information  has been  associated is  a legal  typed
expression of type LISPOB; thus the  set of typed expressions is a  strict
extension of the set of ordinary lisp expressions.

(2) Type of  a compound expression:   The type  of "(C a1  ... an)"  [lisp
syntax], is computed in a simple way from the types of a1 ... an, and of C
- unless C is a special constructor  (such as cond, quote, etc).  If C  is
not a special constructor,  then the rule  is this:  (a) If  C is of  type
function(tp0,tp1 . . . tpn), then a1 . . . an had better be of types  tp1
. . . tpn;  in this case the  type of the  expression (C a1 .  . an) as  a
whole is tp0.  (b) If C is of type  LISPOB, then a1 . . an had all  better
be of type LISPOB, and  the type of the  whole expression is also  LISPOB.
(This is the manner in which a rule given earlier is implemented -  namely
the rule to  the effect  that ordinary  lisp expressions  should be  legal
typed expressions of type LISPOB.)

Each special constructor C has its own rule for determining the
type of an expression in which it appears.  A complete list of constructors
together with their typing rules is given in a later section.

We will, however,  describe two of the special constructors
at this point; these are constructors which do not appear in ordinary
lisp and whose purpose is explicit assignment of new types to
expessions.

Type modification 

(a) type  coercion.  One type tp1  is said to coerce  to
another type tp2 is there  is a chain of  injection maps (declared by  the
mkinjmap operator  described above)  which  leads from  tp1 to  tp2.   The
composition of these maps constitutes  a meaning preserving function  from
tp1 to tp2 - that  is, a map which takes  a representation of an  abstract
object according to the representation scheme of tp1 into a representation
of an abstract object according to  the representation scheme of tp2  such
that the former and the  latter abstract objects are  one in the same.   A
typed expression of the  form "(type E tp)"  (or, in cgol syntax,  "E:tp")
constitutes an instruction to coerce E to type tp.  This can be done  only
when the type of E coerces to tp; if this condition is met, then E:tp is a
legal typed expression of type tp, and  otherwise it is not a legal  typed
expression.

Type coercion is also done auomatically in the process of matching argument types
to function types (though, in our description of this process above, we
avoided mention of this to avoid premature complication).  That is,
an expression (f a1 . . an), where f is of type (function tp0 tp1 . . tpn),
is a legal typed expression if the type of ai coerces to tpi, for 1 ≤ i ≤ n.

(b) Changing levels of abstraction

Let E be of type tp1, and suppose that tp1 represents tp2.
Then "(assigntype E tp2)" is a legal typed expression of type
tp2.  In cgol, "as" is defined as an infix operator with meaning
"assigntype", so that the cgol syntax for "(assigntype E tp2)"
is "E as tp2". The significance of "E as tp2" is that the 
type of E is being lifted to a more abstract level.
E as it stands denotes an object of type tp1; by hypothesis,
objects of type tp1 are the (comparatively) concrete representations
of abstract objects of type tp2.  "E as tp2" denotes the object
of type tp2 which is represented by the denotation of E.

The assigntype operation is more general than this: it allows  expressions
to be viewed at a  level which is more concrete  as well as more  abstract
than its given type.  Any typed  expression denotes objects of types  less
abstract than its assigned type  (unless that type is already  primitive),
since in  the end  objects of  all  types are  represented by  objects  of
primitive type by the mediation of a series of representation maps.  Again
let E be of  type tp1, and  suppose that tp2 represents  tp1.  Then "E  as
tp2" is a legal  typed expression of  type tp2; it  denotes the object  of
type tp2 which E employs to represent its value.

There is yet one more level of generality in the assigntype operation:  it
allows  arbitrary  changes  in  the  level  of  abstraction  at  which  an
expression is viewed.  If tp1 is the type of E, then "E as tp2" is a legal
expression of type tp2  if either tp1 hereditarily  represents tp2, or  if
tp2 hereditarily  represents  tp1.  (Here  tpx  is  said  to  hereditarily
represent tpy if there is a chain of types tp1 . . tpn such that tp1 = tpx
and tpn = tpy, and tpi represents tpi+1).

(c) Transporting information in and out of type world.
One of the design principles of the type system was that it
should not force types on the user against his will.
Therefore an escape mechanism has been provided: a method for
switching the type of a typed expression to lispob (so that
it can be then be manipulated by ordinary lisp code), and a method
for regarding an ordinary lisp value as an object
 of arbitrarily abstract type.
The conversion only applies to pure "data types" - that is types
whose definition at no point involves the use of the "function" construct.
The same constructor is used for this kind of type switching as
is used for changing abstraction level, namely the assigntype operator.
"E as lispob" is always a legal expression of type lispob, regardless
of the type of E.  The value which this expression denotes is defined
as follows.  Let tp be the type of E.  
First suppose that tp is primitive.  Then the value of "E as lispob"
is gotten simply by replacing all tupling operations involved
in building up the value of E by the lisp operation "LIST".
Formally, we define a conversion operation c(x) 
between objects x of primitive data type tp and lisp s-expressions
as follows.


c(x) = x 	if tp is one of the atomic primitive types fixnum,flonum,lispob;
		these  three types ARE lisp objects, so no conversion is needed.

c(x) = list(c(x↓1),c(x↓2) . . c(x↓n))

		if tp = tuple(tp1 . . tpn), where tp1 . . tpn
		and x↓1 . . x↓n are the components of the tuple x.

Then the value of "E as lispob" is just c(x), where x is the value of E.

For the other case, suppose that the type tp of E is not primitive.
Let tp' be the primitive
type which hereditarily represents tp.  Then the value of "E as lispob"
is just "(E as tp') as lispob".  

Going the other way is just a matter of reversing the process.
Let E be of type lispob, and let tp be a primitive type.
Let v be the value of E. If there is any object x of type
tp such that c(x) = v, then that object will be unique,
and then the value of (E as tp) will be v.  If no such x exists,
the value of (E as tp) will be undefined (in evaluation
of (E as tp) in this case, an error will be generated, depending
on the mode of execution).  
For the case where tp is not primitive,
we define "(E as tp)" to be "(E as tp') as tp", where tp' is the
primitive type which hereditarily represents tp.

Polymorphic functions.

The type system includes a very simple kind of polymorphic type
facility.  A polymorphic function is introduced by the operation

dfpfun(f,g1, . . gn)


Here, f is an arbitrary lisp symbol, and g1 . . . gn should
be typed functions introduced earlier by the settyp or dftfun operations,
or else previously defined polymorphic functions.
The effect of this definition is that f "stands for" any one of
the g1 . . gn, depending on the types of the expressions to which it
is applied.  If E is a typed expression in which 
f(a1... an) appears, then f(a1 . . an) is well typed if
there is some gi such that gi(a1 . . an) is well typed.  If the gi
is unique among g1 . . gn, then the  expression
f(a1 . . an) is equivalent to gi(a1 . . an).  If more than one
gi results in a successful type match, then f(a1 . . an) is equivalent
to the first gi in the list for which gi(a1 . . an) is well typed.
(Since each gi might itself be polymorphic, this is a recursive defintion.)
This facility allows one to use the same symbol (eg "+") to designate
operations on several different types (eg integers, reals, vectors
etc).

Conversion to lisp code
When a dffun or teval is executed, the typed expression which
forms the body or argument to the operation is checked to see that
it is well typed, and then converted - or compiled - into a lisp expression.
In the case of dftfun the resulting expression becomes the body
of the expr property of the function symbol, and in the case
of teval, the expression is evaluated and the value, labeled by its
type, is returned.
In future there will be two modes of conversion, though only one
has been implemented so far.  The first (and implemented) conversion
is practically the identity.  The main changes made by the conversion
are these:
(1) wheneever an expression E must be coerced to type
tp, the series of operations which perform the coersion is inserted
into the code.
(2) Assigntype operations (except for conversions to and from
lispob - the escape operations) are no-ops, and are dropped.
(3) Polymorphic function symbols are replaced by the appropriate typed function.
(4) Various constructors which do not appear in ordinary lisp,
such as the tuple selectors and constructors, and the lett construct,
are expanded out in the appropriate way.

In this first conversion method, tuples are represented by lists according
to the scheme given earlier for computing the value of an expression
of the form "(E as lispob)".  As a consequence of this simple representation,
and the simple nature of the conversion,tracing and debugging
of the converted code should be relatively straight-forward.

In the second, yet-to-be-implemented method, tuples will be represented
by collections of variables, array locations, and the like, so that
no consing will be necessary; this should lead to very efficient,
but somewhat obscure, lisp code.
List of constructors for typed expressions

PROG

(type (prog (typed-var-list) e1 . . . en) tp) [lisp syntax]
(prog typed-var-list; e1; . . .  en):tp  [cgol syntax]

Converts to an ordinary lisp prog.  If  the prog
is not explicitly assigned a type, then it will be assigned the type
lispob.  All expressions appearing as arguments to RETURNs within
the scope of this PROG must coerce to the assigned type.  If lispob
does not convert to the assigned type, then "falling off the end"
of the prog (without an explicit return) generates an error (just
returning nil is impossible, because its of the wrong type).


PROGN

(progn e1 . . en) [lisp syntax]
(e1; . . . en)  [cgol syntax]

Converts to an ordinary lisp progn.  The progn expression is assigned
the type of en.

(lett (setq x1 e1)(setq x2 e2) . . . (setq xn en) en+1)  [lisp syntax]
lett(x1 := e1,x2 := e2 . . . xn:=en-1,en)

This is like the maclisp let.  xi is bound in each of ei+1 . . . en
and is assigned the type of ei in its bound appearances.  This converts to
(λ (x1) (λ (x2) ... λ (xn) en+1) en) en-1) . . . e1), which effects a
sequential binding of e1 . . . en to x1 . . xn followed by evaluation of en+1.
The type of the expression is of course just the type of en+1.


TYPE
(type E tp)  [lisp syntax]
 E:tp 	     [cgol syntax]


coerces E to type tp (described in detail above)


ASSIGNTYPE
(assigntype E tp)  [lisp syntax]
E as tp 	     [cgol syntax]

changes the abstraction level of E to tp (described in detail above)
If assigntype has more than two arguments, then it takes on a different
meaning which was not described earlier. 
The other kind of assigntype operation makes it possible to
change the abstraction level of variables within a given typed term.
The form of this other kind of operation is
assigntype(<v1,tp1,v2,tp2, . . . vn,tpn,body>.  
v1 .  . vn should 	be variables bound in the current context.  tp1 . . tpn are
the new types to be assigned to the variables in body. 
Unlike the two argument form, this form cannot be used to 
move values into and out of the type system; rather the purpose
is only that of changing abstraction level.  The assigned types must
lie above or below the original types in the abstraction heirarchy.


COND

(cond (c1 v1)(c2 v2) . . (cn vn))   [lisp syntax]
if c1 then v1 else v2 (for "(cond (c1 v1)(t v2))") [cgol syntax]

Converts to ordinary lisp cond.  v1 . . vn must coerce to a common type,
which is the type of the cond expression.
c1 . . cn must each convert to type boole.  

SETQ

(setq x v) [list syntax]
x:=v	   [cgol syntax]

Converts to an ordinary lisp setq.
The type of the variable x is computed in the general way described above.
v must coerce to the type of x.  


TUPLE

(tuple e1 . . . en) [lisp syntax]
tuple(e1, . . en)   [cgol syntax]

Converts to (list e1  . . . en)  [under first conversion method; see above]
The type of the tuple expression is tuple(tp1 . . tpn), where
tp1 . . . tpn are the types of e1 . . . en.

TSEL  (tuple select)

(TSEL E n)  [lisp syntax]
tsel(E,n)	  [cgol syntax]


E must be an expression of type tuple(tp0 . . . tpk), and n must
be a fixnum constant (not a number valued expression, but a constant,
like "2" or "3").   The arity k+1 of the tuple should be strictly greater
than k.  Like "nth" in lisp, the indexing starts from 0, so that
tsel(E,0) selects the first element of the tuple.  The value of the expression
is the n-1th element of the tuple which is the value of E, and its type
is tpn.  Converts to nth(n,E) under the first conversion method.

That's all for now; other constructs will be added as the need arises,
and will be documented here as they are implemented.
List of type system operations:

described earlier:

tp represents sym   

dftyp(sym,tp)



settyp(sym,tp1, . . tpn)

[remark.  settyp can be used to assign multiple types to a lisp function.
If each of the types tp1 . . tpn is a function type, then the function
designated by sym is polymorphic in the sense
that it is regarded as having each of these types.  The effect of this
is that an appearance f(a1 . . an) of f in a typed expression, 
is well typed if <a1 . . an> can be coerced to the argument types
of any one of f's assigned types.  The possibility of assigning
multiple types to the same function is used primarily in connection
with basic maclisp functions such as =, which are representations
of functions which operate on a variety of abstract types.  Symbols
cannot be assigned multiple data (ie non-functional types), nor a combination
of functional and data types.]

dftfun(sym(varlist),body)

Actually, a dftfun is more general than indicated earlier.  The more general
form is dftfun(f1(varlist1),f2(varlist2) . . fn(varlistn),body).
This results in n functions f1 . . . fn being defined.  Each of
the bodies of the functions is gotten by typing and converting the 
last argument "body" to the dftfun; the resulting code will in general
be different due to the different type assignments which may be made
in the different variable lists varlist1 . . varlistn.  For examples
of use, see geom2d.cgl[hs,ssa].

mkinjmap(tp1,tp2,f)

teval(exp)


dfpfun(f,g1 . . gn)  polymorphic function definition



Not described earlier:

mktupletyp(sym,subtypes,constructor,selectors)

			This is a macro which expands out to a series
			of type operations.
			here, sym is the name of the new type being
			introduced.  The effect of the operation
			is to define sym as a type whose elements are
			represented by tuples with components of types
			given by subtypes.
			constructor is the name assigned to the
			construction function for elements of the new
			type.  selectors is a list of the names
			of the selection functions on the new type.
			Note that, if subtypes = (sb1 . . sbn),
			that sym is not the same type as (tuple sb1 . . sbn);
			rather, (tuple sb1 . . sbn) REPRESENTS the new type sym.


addpfuns(f,g1 . . gn)   

	add g1 . . gn to the list of alternatives for the polymorphic
	function f.  g1 . . gn are added to the front of the list
	of f's alternatives

addtyps(sym,tp1, . . tpn)

	add tp1 . . .tpn to the list of alternative types for sym.
	tp1 . . tpn must all be functional types.

tsetq(sym,E)

	sym is lisp symbol, and E is a typed expression.  This
	has the effect of setting the value of sym to the value of
	(E as lispob), and the type of sym to the type of E.
	It constitutes a kind of global typed setq.

dftmacro(sym(varlist),body)
	
Macros which are to be used in type world should be defined by
the dftmacro (define macro for type world) facility.  
No type information is associated with the macro; a macro, after all,
operates on code, not on what the code represents, so no type
restrictons should apply to the code passed to a macro.  
The macro is expanded at type assignment time, so it should return
a well typed expression as value.  The manner of expansion is
identical to that of ordinary macros in lisp: the
macro code is applied to the expression containing the invocation of
the macro, and the result returned takes the place of that expression.
One common
role of macros in LISP, namely, defining open coded functions,
is handled by a separate facility:
the dftopen operation. 

dftopen(sym(typedvarlist),body)
dftopenopt(sym(typedvarlist),body)

	these have effects similar to that of dftfun, but
	define sym as an "open coded" function.
	An open coded function is one whose
	invocation in type system code will be
	replaced by its body with the appropriate substitutions
	done - that is, it is a function whose invocations
	are open coded in the usual sense.  The open coding
	is done at the time that the typed code containing
	the invocation is converted into lisp.  Two further
	details need mentioning:
	(1) How the open coding is done.  If "f(a1 . . an)"
	appears in typed code, then it is replaced
	by either the result of substituting a1, . . an for
	the input variables in the body of f, or by
	an expression of the form (λvarlist;body)(arglist).
	The first alternative is taken if all of the ai are atomic,
	and the second otherwise [this policy prevents repeated
	evaluation of the arguments, if that evaluation is non-trivial].
	(2)  A dftopen always does an ordinary dftfun as well as
	setting up for the open coding operations described above.
	Thus, in the course of converting a piece of typed code
	it is not essential that invocations of open coded
	functions actually be open coded.  Whether or not open coding
	is done is controlled by the switches "typesystemopencode",
	and "typesystemopencodeeverything", and finally the list
	"typesystemopencodelist".  The rules for whether open coding
	is done are as follows:
	(a) If typesystemopencode is nil, then no open coding at all
	is done. 
	(b) If typesystemopencode is t, then all functions defined
	by dftopen are coded.  The other two globals control
	open coding of functions defined by dftopenopt ("define
	open coded function, optional").  If typesystemopencodeeverything"
	is t, then all optionally open coded functions are open coded.
	Otherwise, exactly those optionally open coded 
	functions whose names appear
	in the list typesystemopencodelist are open coded.

	A similar facility for open coding in ordinary functions
	(non type system functions) exists; for details see
	the description of dfopen in dfmacs.cgl[imp,ssa].

Compiling typed code.

The type system is set up in such a way that typed code
can be fed directly to the compiler, with the result
that the  fasl files generated have equivalent effects
to the original uncompiled files.  It should be kept in mind,
however,  a typed function definition requires that
the types of all functions appearing in the definition be known
when the definition is done, and that the code for
all open coded function be available.  This data needs to
be available in the compiler when dftfuns are compiled.
Thus, before a given file is compiled, all files containing
defintions of functions referred to in that file need to be
loaded into the compiler.  Aid in ensuring this is provided by
the trequire facility, described earlier.
The other type constructors: list and union.

If tp, tp1,  . . tpn are type expressions, then
list(tp) and union(tp1. . . tpn) are type expressions.
The arguments tp1 . . tpn to union should be distinct types
(although their classes need not be disjoint, or indeed, distinct).

The types which they denote are as follows.
class(list(tp)) is simply the set of all lists of elements of type
tp.  
rep(list(tp)) is just list(rep(tp)), unless tp is primitive, in
which case list(tp) is primitive too.
repmap(list(tp)) is λx(mapcar(function(repmap(tp))(x))); that is
the representation map just takes a list of representatives and
maps them, mapcar style, into the list of what they represent.

In describing the meaning of union, we need to introduce
the disjoint union type constructor.
As will be seen,
in the implementation of the type system, one constructor
(called "union") serves for both union and disjoint union.
But a precise explanation of what's going on requires that the
distinction be made at this point.  We introduce disjoint union first.


If tp0, . . tpn are types then dunion(tp0, . . tpn) is a type.
class(dunion(tp0 . . tpn)) is defined in a conventional way; the members
of the class are members of the union of the classes of tp1 . . tpn,
marked so as to indicate which one of tp0 . . . tpn they came from.
It doesn't much matter what the marking system is, but for the
sake of concreteness, we define class(dunion(tp0 . . tpn))
as C0 ∪ C1 . . ∪ Cn, where  Ck = {x|x = tuple(k,y) for some y in class(tpk)}.
rep(dunion(tp0, . .tpn)) = dunion(rep(tp0) . . rep(tpn)),
unless tp0 . . tpn are primitive, in which case, dunion(tp0  . tpn) is too.
f=repmap(dunion(tp0 . . tpn)) is defined by
f(tuple(k,y)) = tuple(k,repmap(tpk)(y)); that is the representation
map looks at the label to see which element of the disjoint union
its argument is in, and uses the appropriate representation map to determine
what it represents, and finally sticks the label back on.

Now for union.
class(union(tp0 . . tpn)) = tp0 ∪ tp1 . . tpn.
rep(union(tp0 . . tpn)) = dunion(tp0 . . tpn)
f=repmap(union(tp0 . . tpn))  is defined by
f(tuple(k,y)) = y; that is, the representation map just removes the
label.

In practice, it is not necessary to implement a separate
disjoint union type.  This is because every typed term, as explained earlier,
denotes a tower of representations, from the primitive type up to its assigned
type, where each item in the tower represents the item one level up 
through the representation map of the type at the next level up.
In particular a typed term of type union denotes a tower of representations
where the item next to the top of the tower is an item of the corresponding
disjoint union.  We do not bother to allow the creation of terms
whose denotations are representation towers which stop at the disjoint
union level, and do not extend up to the union; however, two of
the three operations on terms of union type actually, strictly speaking,
operate on their representations as disjoint unions.  We do not need
to make this explicit, since each operation operates either on the
union type or the disjoint union type, and never both, so there is no
ambiguity.

The operations on union types are these:

uinj(x,tp)  injects x into the union type tp.  tp should have
 	    the form union(tp0 . .tpn), and x should have type tpk
	    for some k. uinj(x,tp) is
	    of type union(tp0, .. . tpn), and denotes
	    the same object as x.  The representation of uinj(x,tp)
	    in dunion(tp0 . . tpn) is tuple(k,x).

uproj(x,tp) projects x out of a union type into a subtype.
	    here, x should be of type union(tp0 . . .tpn), where
            tp = tpk for some k.  This is really an operation
            on dunion(tp0 . . tpk), although, for the reasons given
	    above, this distinction is not explicitly made.
            x, as a member of dunion(tp0 . . . tpn) will have
	    the form tuple(k,y) where y is in tpk.  Now,
	    if tp = tpk, then uproj(x,tp) = y.  Otherwise,
	    uproj(x,tp) is undefined. The policy in the type system is to
	    let the user watch out for himself in any situation where
     	    having the system watch out for him would slow things down.
	    In particular, run time checks are avoided.  In keeping
	    with this policy, whenever uproj(x,tp) is invoked and
	    its result is undefined, then its result will really be
	    undefined in the implementation; the value of the invocation
	    is random garbage which may produce errors later.

umem(x,tp)  checks an element of a union type for membership in a subtype.
	    x should be of type union(tp0 . . tpn), where tp = tpk
	    for some k.  Again, this is really an operation on 
	    dunion(tp0 . . . tpn).   x as a member of
  	    dunion(tp0 . . tpn) will have the form tuple(j,y).
	    If j = k then umem(x,tp) is TRUE, otherwise it is FALSE.

Automatic coercion of members of subtypes into union types is supported.
That is, whenever a term of type tpj appears where a term
of type union(tp0. . tpn) is expected, the term will be automatically
coerced (by a uinj) to the right type.

Operations on lists.

The operations on list types are a subset of the lisp operations
on lists, with corresponding meanings.  The operations currently supported
are:

list,nth,append,cons,reverse,nreverse, 
cars and cdrs unto the fourth generation (up to 4 a's and d's between "c" and "r")

In addition, there are two new operations.
(1) emptylist(tp);  creates an empty list of type list(tp); this
		    cannot be done with "list"; which must have at least
		    one argument.
(2) lsel(x,k);	    this is the same as nth with arguments reversed -
		    matches the syntax of tsel (tuple sel).
File management: the  "require" and "doneloading" operations.

The typesystem includes a very simple file management facility.
A global variable "typefilesloaded" is maintained, which
is used in the two file management operations.

(1) doneloading(x) is a macro which simply adds x (unquoted)
    to the list "typefilesloaded".  Typically, this oeeration
    should be placed at the end of type files, with the name
    of the file itself as argument.

(2) require(filename1 . . filenamen) is a macro which
    loads each of the files in the list of arguments to which
    it is applied, except those which are listed in the
    typefilesloaded list.  typefilesloaded is updated by
    adding the names of the loaded files.

Use of the type system in the SSA environment, and pointers to examples.

The elisp.ini file on the SSA area - which controls the intialization
of lisp subjobs - reads in the file type.ini, which has
responsibility for setting up for the type system.
So at, the moment, when a lisp subjob is initialized, the type
system is initialized as well. Two files which contain
definitions of a number of basic types, and which may be inspected
for examples of the use of the type system, are
arith.cgl[hs,ssa] (basic arithmetic)
geom2d.cgl[hs,ssa] (2d geometry).

DFMACS.CGL[imp,ssa] contains macros for ordinary lisp versions
of some of the constructs of the type system, such as dfopen,
and lett.